Nuprl Lemma : divides_nchar
2,24
postcript
pdf
a
,
b
:
.
a
|
b
(
c
:
.
b
=
a
c
)
latex
Definitions
b
|
a
,
P
Q
,
P
&
Q
,
P
Q
,
P
Q
,
x
:
A
.
B
(
x
)
,
x
:
A
.
B
(
x
)
,
t
T
,
,
Prop
,
i
>
j
,
P
Q
,
T
,
True
Lemmas
mul
bounds
1b
,
pos
mul
arg
bounds
,
nat
plus
wf
origin
a, b:
. a | b 
(
c:. b = a
c 
) a, b:. a | b (c:. b = ac ) Q
Q Qx:A. B(x)x:A. B(x) T
Q
T